Inference at * 1 
Iof proof for Lemma branch wf:

.....subterm..... T:t1:n

1. P : 
2. d : Dec(P)
3. T : Type
4. PT
5. T
  d  (P + (P)) 

latex

 by ((Fold `or` 0) 
CollapseTHEN (Fold `decidable` 0)) 
CollapseTHEN (Auto) 

latex

C.

Definitions

t  T